/*

eXamine Modeling Operations

*/
open core

// Add sub-component
pred addComponent [ s, s' : System, p, c : Component ] {
	// pre-conditions
	c not in s.getComponents
	p in s.childs.Component
	// change state
	s'.childs = s.childs + (p -> c)
	// Frame conditions
	s'.failures = s.failures
}

pred pos_addComponent [ s : System, p, c : Component ] {
	c in p.(s.childs)
}

assert verify_addComponent {
	all s, s' : System |
		all p : s.getComponents |
			all c : Component | s.invSystem && s.addComponent[s', p, c] => s'.invSystem && s'.pos_addComponent[p, c] 
}

check  verify_addComponent for 5
run addComponent for 5

// Add failure
pred addFailure [ s, s' : System, p : Component, f : Failure ] {
	// Pre-conditions
	f not in s.getFailures[s.getComponents]
	f.received in (
		// 2.1
		(f.received & ReceivedEvent) +
		// 2.2
		s.getThrownEvents[s.getChilds[p]] +
		// 2.3
		s.getThrownEvents[s.getSameLevel[p]]
	)
	some f.received
	no ((f.received & ReceivedEvent) & (s.getReceivedEvents[s.getComponents - p] & ReceivedEvent))
	no (f.thrown & s.getThrownEvents[s.getComponents - p])
	// 3
	isDag[s, f]
	// change state
	s'.failures = s.failures + (p -> f)
	// Frame conditions
	s'.childs = s.childs
}

pred pos_addFailure [ s : System, p : Component, f : Failure ] {
	f in s.getFailures[p]
}

assert verify_addFailure {
	all s, s' : System |
		all p : s.getComponents |
			all f : Failure | s.invSystem && s.addFailure[s', p, f] => s'.invSystem && s'.pos_addFailure[p, f] 
}

check  verify_addFailure for 5 but exactly 2 System
run addFailure for 5
